\begin{tabbing}
$\forall$$D$:Dsys, $L$:Id List, $f$:(Id$\rightarrow$Type).
\\[0ex]($\forall$$i$:Id. ($i$ $\in$ $L$) $\vee$ M($i$) $=$  $\in$ MsgA)
\\[0ex]$\Rightarrow$ (\=$\forall$$i$$\in$$L$.\+
\\[0ex]$\forall$$l$:IdLnk, ${\it tg}$:Id. rcv($l$,${\it tg}$) declared in M($i$) $\Rightarrow$ M($i$).da(rcv($l$,${\it tg}$)) $=$ $f$(${\it tg}$) $\in$ Type)
\-\\[0ex]$\Rightarrow$ ($\forall$$i$:Id. Feasible(M($i$)))
\\[0ex]$\Rightarrow$ Feasible($D$)
\end{tabbing}